T1,T2:Type, r1:(T1T1), r2:(T2T2).
(T1 = T2)
 (x,y:T1. {r1(x,y)  r2(x,y)})
 {WellFnd{i}(T1;x,y.r1(x,y))  WellFnd{i}(T2;x,y.r2(x,y))} 

latex

ProofTree

Definitions	t  T, x(s), WellFnd{i}(A;x,y.R(x;y)), x(s1,s2), P  Q, {T}, P  Q, , x:A. B(x), x. t(x)
Lemmas	rev implies wf, guard wf